On the (infinity,1)-Grothendieck construction via straightening and unstraightening entirely within the context of quasi-categories:
On the resulting interpretation of the universal coCartesian fibration as categorical semantics for a univalent type universe in directed homotopy type theory:
On the directed univalence axiom in this context:
Last revised on May 11, 2023 at 08:48:28. See the history of this page for a list of all contributions to it.